R:Realizer. R-Feasible(R)  (es:ES. Consistent(R;es)) 

latex

Definitions	t  T, P  Q, x:A. B(x), Consistent(R;es), P  Q, x:A. B(x), x:AB(x), x:AB(x), R-Feasible(R), ES, P & Q, P  Q, Realizer
Lemmas	R-Feasible-possible, es realizer wf, R-Feasible wf, R-consistent wf, R-possible-Rconsistent